Nuprl Lemma : grp_op_r
13,42
postcript
pdf
g
:GrpSig,
a
,
b
,
c
:|
g
|. (
a
=
b
)
((
a
*
c
) = (
b
*
c
)
|
g
|)
latex
Up
groups
1
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
f
y
Lemmas
grp
sig
wf
,
grp
car
wf
,
grp
op
wf
origin
g:GrpSig, a, b, c:|g|. (a = b) 
((a * c) = (b * c) 
|g|) g:GrpSig, a, b, c:|g|. (a = b) ((a * c) = (b * c) |g|) 
T Qx:A. B(x)